Termination Proof Script

Consider the TRS R consisting of the rewrite rules


1:		app(nil,YS)	→ YS
2:		app(cons(X,XS),YS)	→ cons(X,app(XS,YS))
3:		from(X)	→ cons(X,from(s(X)))
4:		zWadr(nil,YS)	→ nil
5:		zWadr(XS,nil)	→ nil
6:		zWadr(cons(X,XS),cons(Y,YS))	→ cons(app(Y,cons(X,nil)),zWadr(XS,YS))
7:		prefix(L)	→ cons(nil,zWadr(L,prefix(L)))

There are 6 dependency pairs:


8:		APP(cons(X,XS),YS)	→ APP(XS,YS)
9:		FROM(X)	→ FROM(s(X))
10:		ZWADR(cons(X,XS),cons(Y,YS))	→ APP(Y,cons(X,nil))
11:		ZWADR(cons(X,XS),cons(Y,YS))	→ ZWADR(XS,YS)
12:		PREFIX(L)	→ ZWADR(L,prefix(L))
13:		PREFIX(L)	→ PREFIX(L)

The approximated dependency graph contains 4 SCCs: {8}, {9}, {11} and {13}.

Consider the SCC {8}. There are no usable rules. By taking the AF π with π(APP) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 8 is strictly decreasing.

Consider the SCC {9}. There are no usable rules. The constraints could not be solved.

Consider the SCC {11}. There are no usable rules. By taking the AF π with π(ZWADR) = 1 and π(cons) = [2] together with the lexicographic path order with empty precedence, rule 11 is strictly decreasing.

Consider the SCC {13}. There are no usable rules. The constraints could not be solved.

Tyrolean Termination Tool (0.01 seconds) --- May 4, 2006